/* Benchmarks for the PionterC verifier. */

// inductive definition example

struct node
{
  int data;
  struct node* next;
};

/*@ let any_definition(l) = (true && true || false)
  @ in  any_definition(l)
  @ end
  @*/

struct node* test(struct node* n)
{
  // function body
  return n;
}
/*@  */
